1  /-
  2  Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Sébastien Gouëzel
  5  -/
  6  
  7  import analysis.convex.basic analysis.normed_space.bounded_linear_maps analysis.specific_limits
src         └───────────────────┘ └───────────────────────────────────────┘ └──────────────────────┘
  8  
  9  /-!
 10  # Tangent cone
 11  
 12  In this file, we define two predicates `unique_diff_within_at 𝕜 s x` and `unique_diff_on 𝕜 s`
 13  ensuring that, if a function has two derivatives, then they have to coincide. As a direct
 14  definition of this fact (quantifying on all target types and all functions) would depend on
 15  universes, we use a more intrinsic definition: if all the possible tangent directions to the set
 16  `s` at the point `x` span a dense subset of the whole subset, it is easy to check that the
 17  derivative has to be unique.
 18  
 19  Therefore, we introduce the set of all tangent directions, named `tangent_cone_at`,
 20  and express `unique_diff_within_at` and `unique_diff_on` in terms of it.
 21  One should however think of this definition as an implementation detail: the only reason to
 22  introduce the predicates `unique_diff_within_at` and `unique_diff_on` is to ensure the uniqueness
 23  of the derivative. This is why their names reflect their uses, and not how they are defined.
 24  
 25  ## Implementation details
 26  
 27  Note that this file is imported by `fderiv.lean`. Hence, derivatives are not defined yet. The
 28  property of uniqueness of the derivative is therefore proved in `fderiv.lean`, but based on the
 29  properties of the tangent cone we prove here.
 30  -/
 31  
 32  variables (𝕜 : Type*) [nondiscrete_normed_field 𝕜]
id                          └──────────────────────┘
src                         └──────────────────────┘
typ                         └──────────────────────┘
doc                         └──────────────────────┘
 33  variables {E : Type*} [normed_group E] [normed_space 𝕜 E]
id                          └──────────┘     └──────────┘
src                         └──────────┘     └──────────┘
typ                         └──────────┘     └──────────┘
doc                         └──────────┘     └──────────┘
 34  variables {F : Type*} [normed_group F] [normed_space 𝕜 F]
id                          └──────────┘     └──────────┘
src                         └──────────┘     └──────────┘
typ                         └──────────┘     └──────────┘
doc                         └──────────┘     └──────────┘
 35  variables {G : Type*} [normed_group G] [normed_space ℝ G]
id                          └──────────┘     └──────────┘ 
src                         └──────────┘     └──────────┘ 
typ                         └──────────┘     └──────────┘ 
doc                         └──────────┘     └──────────┘
 36  
 37  set_option class.instance_max_depth 50
doc             └──────────────────────┘
 38  open filter set
 39  open_locale topological_space
 40  
 41  /-- The set of all tangent directions to the set `s` at the point `x`. -/
 42  def tangent_cone_at (s : set E) (x : E) : set E :=
id                            └─┘            └─┘ 
src                           └─┘              └─┘
typ                           └─┘            └─┘ 
 43  {y : E | ∃(c : ℕ → 𝕜) (d : ℕ → E), (∀ᶠ n in at_top, x + d n ∈ s) ∧
id                             └┘  └┘ └────┘        
src                                 └┘   └┘ └────┘            
typ                            └┘  └┘ └────┘        
doc                                      └┘   └┘ └────┘
 44    (tendsto (λn, ∥c n∥) at_top at_top) ∧ (tendsto (λn, c n • d n) at_top (𝓝 y))}
id      └─────┘        └────┘ └────┘    └─────┘           └────┘   
src     └─────┘           └────┘ └────┘    └─────┘                └────┘  
typ     └─────┘        └────┘ └────┘    └─────┘           └────┘   
doc     └─────┘             └────┘ └────┘     └─────┘                 └────┘  
 45  
 46  /-- A property ensuring that the tangent cone to `s` at `x` spans a dense subset of the whole space.
 47  The main role of this property is to ensure that the differential within `s` at `x` is unique,
 48  hence this name. The uniqueness it asserts is proved in `unique_diff_within_at.eq` in `fderiv.lean`.
 49  To avoid pathologies in dimension 0, we also require that `x` belongs to the closure of `s` (which
 50  is automatic when `E` is not `0`-dimensional).
 51   -/
 52  def unique_diff_within_at (s : set E) (x : E) : Prop :=
 53  closure ((submodule.span 𝕜 (tangent_cone_at 𝕜 s x)) : set E) = univ ∧ x ∈ closure s
 54  
 55  /-- A property ensuring that the tangent cone to `s` at any of its points spans a dense subset of
 56  the whole space.  The main role of this property is to ensure that the differential along `s` is
 57  unique, hence this name. The uniqueness it asserts is proved in `unique_diff_on.eq` in
 58  `fderiv.lean`. -/
 59  def unique_diff_on (s : set E) : Prop :=
 60  ∀x ∈ s, unique_diff_within_at 𝕜 s x
 61  
 62  variables {𝕜} {x y : E} {s t : set E}
 63  
 64  section tangent_cone
 65  /- This section is devoted to the properties of the tangent cone. -/
 66  
 67  open normed_field
 68  
 69  lemma tangent_cone_univ : tangent_cone_at 𝕜 univ x = univ :=
 70  begin
 71    refine univ_subset_iff.1 (λy hy, _),
src    └─────┘               └─┘  └──────┘
typ    └─────┘               └─┘  └──────┘
doc    └─────┘               └─┘  └──────┘
txt    └─────┘               └─┘  └──────┘
par    └─────┘               └─┘  └──────┘
pid                         └─┘  └──────┘
 72    rcases exists_one_lt_norm 𝕜 with ⟨w, hw⟩,
src    └─────┘                   └───────────┘
typ    └─────┘                   └───────────┘
doc    └─────┘                   └───────────┘
txt    └─────┘                   └───────────┘
par    └─────┘                   └───────────┘
pid                             └───────────┘
 73    refine ⟨λn, w^n, λn, (w^n)⁻¹ • y, univ_mem_sets' (λn, mem_univ _),  _, _⟩,
src    └─────┘  └─┘   └┘ └─┘        └┘                └─┘        └─────────┘
typ    └─────┘  └─┘   └┘ └─┘        └┘                └─┘        └─────────┘
doc    └─────┘  └─┘   └┘ └─┘        └┘                └─┘        └─────────┘
txt    └─────┘  └─┘   └┘ └─┘        └┘                └─┘        └─────────┘
par    └─────┘  └─┘   └┘ └─┘        └┘                └─┘        └─────────┘
pid            └─┘   └┘ └─┘        └┘                └─┘        └─────────┘
 74    { simp only [norm_pow],
src      └─────────┘        
typ      └─────────┘        
doc      └─────────┘        
txt      └─────────┘        
par      └─────────┘        
pid          └──┘└┘        
 75      exact tendsto_pow_at_top_at_top_of_gt_1 hw },
src      └────┘                                   
typ      └────┘                                   
doc      └────┘                                   
txt      └────┘                                   
par      └────┘                                   
pid                                              
 76    { convert tendsto_const_nhds,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid             
 77      ext n,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid         └┘
 78      have : w ^ n * (w ^ n)⁻¹ = 1,
id                             
src      └─────┘         └┘
typ      └─────┘       └┘
doc      └─────┘           └┘
txt      └─────┘           └┘
par      └─────┘           └┘
pid      └───┘└┘           
st               └──────────────────┘└─
 79      { apply mul_inv_cancel,
id               └────────────┘
src        └────┘└────────────┘
typ        └────┘└────────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────┘└──────────────────┘└─
 80        apply pow_ne_zero,
id               └─────────┘
src        └────┘└─────────┘
typ        └────┘└─────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ──────────────────────┘└─
 81        simpa [norm_eq_zero] using (ne_of_lt (lt_trans zero_lt_one hw)).symm },
id                └──────────┘         └──────┘  └──────┘ └─────────┘ └┘
src        └─────┘└──────────┘└──────┘ └──────┘ └──────┘└─────────┘  └──────┘
typ        └─────┘└──────────┘└──────┘ └──────┘ └──────┘└─────────┘└┘└──────┘
doc        └─────┘            └──────┘                               └──────┘
txt        └─────┘            └──────┘                               └──────┘
par        └─────┘            └──────┘                               └──────┘
pid                         └────┘                               └────┘└┘
st   ──────────────────────────────────────────────────────────────────────────┘└┘
 82      rw [smul_smul, this, one_smul] }
id           └───────┘  └──┘  └──────┘
src      └──┘└───────┘└┘    └┘└──────┘└┘
typ      └──┘└───────┘└┘└──┘└┘└──────┘└┘
doc      └──┘         └┘    └┘        └┘
txt      └──┘         └┘    └┘        └┘
par      └──┘         └┘    └┘        └┘
pid        └┘         └┘    └┘        
st   ────────────────┘└────┘└────────┘└─
 83  end
st   ──┘
 84  
 85  lemma tangent_cone_mono (h : s ⊆ t) :
id                                  
src                                 
typ                                 
 86    tangent_cone_at 𝕜 s x ⊆ tangent_cone_at 𝕜 t x :=
id     └─────────────┘     └─────────────┘   
src    └─────────────┘        └─────────────┘
typ    └─────────────┘     └─────────────┘   
doc    └─────────────┘         └─────────────┘
 87  begin
st   └─────
 88    rintros y ⟨c, d, ds, ctop, clim⟩,
src    └──────────────────────────────┘
typ    └──────────────────────────────┘
doc    └──────────────────────────────┘
txt    └──────────────────────────────┘
par    └──────────────────────────────┘
pid           └───────────────────────┘
st   ─────────────────────────────────┘└─
 89    exact ⟨c, d, mem_sets_of_superset ds (λn hn, h hn), ctop, clim⟩
id                └──────────────────┘ └┘               └──┘  └──┘
src    └────┘  └┘ └┘└──────────────────┘    └────┘   └─┘    └┘    └┘
typ    └────┘ └┘└┘└──────────────────┘└┘  └────┘  └─┘└──┘└┘└──┘└┘
doc    └────┘  └┘ └┘                        └────┘   └─┘    └┘    └┘
txt    └────┘  └┘ └┘                        └────┘   └─┘    └┘    └┘
par    └────┘  └┘ └┘                        └────┘   └─┘    └┘    └┘
pid           └┘ └┘                        └────┘   └─┘    └┘    
st   ─────────────────────────────────────────────────────────────────┘
 90  end
st   └─┘
 91  
 92  /-- Auxiliary lemma ensuring that, under the assumptions defining the tangent cone,
 93  the sequence `d` tends to 0 at infinity. -/
 94  lemma tangent_cone_at.lim_zero {α : Type*} (l : filter α) {c : α → 𝕜} {d : α → E}
id                                                   └────┘                     
src                                                  └────┘
typ                                                  └────┘                     
 95    (hc : tendsto (λn, ∥c n∥) l at_top) (hd : tendsto (λn, c n • d n) l (𝓝 y)) :
id           └─────┘         └────┘        └─────┘              
src          └─────┘             └────┘        └─────┘                   
typ          └─────┘         └────┘        └─────┘              
doc          └─────┘               └────┘        └─────┘                    
 96    tendsto d l (𝓝 0) :=
id     └─────┘    
src    └─────┘      
typ    └─────┘    
doc    └─────┘      
 97  begin
st   └─────
 98    have A : tendsto (λn, ∥c n∥⁻¹) l (𝓝 0) := tendsto_inv_at_top_zero.comp hc,
id              └─────┘        └┘           └──────────────────────────┘ └┘
src    └───────┘└─────┘  └─┘  └┘└┘  └─────┘└──────────────────────────┘
typ    └───────┘└─────┘  └─┘ └┘└┘ └─────┘└──────────────────────────┘└┘
doc    └───────┘└─────┘  └─┘      └┘  └─────┘                            
txt    └───────┘         └─┘      └┘   └─────┘                            
par    └───────┘         └─┘      └┘   └─────┘                            
pid    └────┘└─┘         └─┘      └┘   └─┘└──┘                            
st   ──────────────────────────────────────────────────────────────────────────┘└─
 99    have B : tendsto (λn, ∥c n • d n∥) l (𝓝 ∥y∥) :=
id              └─────┘                     
src    └───────┘└─────┘  └─┘      └┘      └────
typ    └───────┘└─────┘  └─┘    └┘    └────
doc    └───────┘└─────┘  └─┘       └┘      └────
txt    └───────┘         └─┘       └┘      └────
par    └───────┘         └─┘       └┘      └────
pid    └────┘└─┘         └─┘       └┘      └───
st   ──────────────────────────────────────────────────
100      (continuous_norm.tendsto _).comp hd,
id        └─────────────────────┘         └┘
src  ───┘ └─────────────────────┘└───────┘
typ  ───┘ └─────────────────────┘└───────┘└┘
doc  ───┘                        └───────┘
txt  ───┘                        └───────┘
par  ───┘                        └───────┘
pid  ───┘                        └───────┘
st   ──────────────────────────────────────┘└─
101    have C : tendsto (λn, ∥c n∥⁻¹ * ∥c n • d n∥) l (𝓝 (0 * ∥y∥)) := A.mul B,
id              └─────┘                                           └───┘ 
src    └───────┘└─────┘  └─┘             └┘    └┘    └────┘└───┘
typ    └───────┘└─────┘  └─┘           └┘   └┘   └────┘└───┘
doc    └───────┘└─────┘  └─┘              └┘    └┘    └────┘     
txt    └───────┘         └─┘              └┘    └┘    └────┘     
par    └───────┘         └─┘              └┘    └┘    └────┘     
pid    └────┘└─┘         └─┘              └┘    └┘    └┘└──┘     
st   ────────────────────────────────────────────────────────────────────────┘└─
102    rw zero_mul at C,
id        └──────┘
src    └─┘└──────┘└───┘
typ    └─┘└──────┘└───┘
doc    └─┘        └───┘
txt    └─┘        └───┘
par    └─┘        └───┘
pid              └───┘
st   ─────────────────┘└─
103    have : ∀ᶠ n in l, ∥c n∥⁻¹ * ∥c n • d n∥ = ∥d n∥,
id            └┘   └┘                         
src    └─────┘└┘└─┘└┘                 
typ    └─────┘└┘└─┘└┘              
doc    └─────┘└┘└─┘└┘                  
txt    └─────┘  └─┘                     
par    └─────┘  └─┘                     
pid    └───┘└┘  └─┘                     
st   ────────────────────────────────────────────────┘└─
104    { apply mem_sets_of_superset (ne_mem_of_tendsto_norm_at_top hc 0) (λn hn, _),
id             └──────────────────┘  └───────────────────────────┘ └┘
src      └────┘└──────────────────┘ └───────────────────────────┘  └──┘  └──────┘
typ      └────┘└──────────────────┘ └───────────────────────────┘└┘└──┘  └──────┘
doc      └────┘                     └───────────────────────────┘  └──┘  └──────┘
txt      └────┘                                                    └──┘  └──────┘
par      └────┘                                                    └──┘  └──────┘
pid                                                               └──┘  └──────┘
st   ───┘└─────────────────────────┘└────────────────────────────────────────────┘└─
105      rw [mem_set_of_eq, norm_smul, ← mul_assoc, inv_mul_cancel, one_mul],
id           └───────────┘  └───────┘    └───────┘  └────────────┘  └─────┘
src      └──┘└───────────┘└┘└───────┘└──┘└───────┘└┘└────────────┘└┘└─────┘
typ      └──┘└───────────┘└┘└───────┘└──┘└───────┘└┘└────────────┘└┘└─────┘
doc      └──┘             └┘         └──┘         └┘              └┘       
txt      └──┘             └┘         └──┘         └┘              └┘       
par      └──┘             └┘         └──┘         └┘              └┘       
pid        └┘             └┘         └──┘         └┘              └┘       
st   ────────────────────┘└─────────┘└───────────┘└──────────────┘└───────┘└──
106      rwa [ne.def, norm_eq_zero] },
id            └────┘  └──────────┘
src      └───┘└────┘└┘└──────────┘└┘
typ      └───┘└────┘└┘└──────────┘└┘
doc      └───┘      └┘            └┘
txt      └───┘      └┘            └┘
par      └───┘      └┘            └┘
pid         └┘      └┘            
st   ──────────────┘└────────────┘└┘
107    have D : tendsto (λ n, ∥d n∥) l (𝓝 0) :=
id              └─────┘             
src    └───────┘└─────┘  └──┘    └┘   └──────
typ    └───────┘└─────┘  └──┘   └┘  └──────
doc    └───────┘└─────┘  └──┘    └┘   └──────
txt    └───────┘         └──┘    └┘   └──────
par    └───────┘         └──┘    └┘   └──────
pid    └────┘└─┘         └──┘    └┘   └─┘└───
st   ───────────────────────────────────────────
108      tendsto.congr' this C,
id       └────────────┘ └──┘ 
src  ───┘└────────────┘    
typ  ───┘└────────────┘└──┘
doc  ───┘                  
txt  ───┘                  
par  ───┘                  
pid  ───┘                  
st   ────────────────────────┘└─
109    rw tendsto_zero_iff_norm_tendsto_zero,
id        └────────────────────────────────┘
src    └─┘└────────────────────────────────┘
typ    └─┘└────────────────────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ──────────────────────────────────────┘└─
110    exact D
id           
src    └────┘ 
typ    └────┘
doc    └────┘ 
txt    └────┘ 
par    └────┘ 
pid          
st   ─────────┘
111  end
st   └─┘
112  
113  lemma tangent_cone_mono_nhds (h : nhds_within x s ≤ nhds_within x t) :
id                                     └─────────┘    └─────────┘  
src                                    └─────────┘      └─────────┘
typ                                    └─────────┘    └─────────┘  
doc                                    └─────────┘       └─────────┘
114    tangent_cone_at 𝕜 s x ⊆ tangent_cone_at 𝕜 t x :=
id     └─────────────┘     └─────────────┘   
src    └─────────────┘        └─────────────┘
typ    └─────────────┘     └─────────────┘   
doc    └─────────────┘         └─────────────┘
115  begin
st   └─────
116    rintros y ⟨c, d, ds, ctop, clim⟩,
src    └──────────────────────────────┘
typ    └──────────────────────────────┘
doc    └──────────────────────────────┘
txt    └──────────────────────────────┘
par    └──────────────────────────────┘
pid           └───────────────────────┘
st   ─────────────────────────────────┘└─
117    refine ⟨c, d, _, ctop, clim⟩,
id                    └──┘  └──┘
src    └─────┘  └┘ └───┘    └┘    
typ    └─────┘ └┘└───┘└──┘└┘└──┘
doc    └─────┘  └┘ └───┘    └┘    
txt    └─────┘  └┘ └───┘    └┘    
par    └─────┘  └┘ └───┘    └┘    
pid            └┘ └───┘    └┘    
st   ─────────────────────────────┘└─
118    suffices : tendsto (λ n, x + d n) at_top (nhds_within x t),
id                └─────┘              └────┘  └─────────┘  
src    └─────────┘└─────┘  └──┘   └┘└────┘ └─────────┘  
typ    └─────────┘└─────┘  └──┘  └┘└────┘ └─────────┘
doc    └─────────┘└─────┘  └──┘    └┘└────┘ └─────────┘  
txt    └─────────┘         └──┘    └┘                    
par    └─────────┘         └──┘    └┘                    
pid    └───────┘└┘         └──┘    └┘                    
st   ───────────────────────────────────────────────────────────┘└─
119      from tendsto_principal.1 (tendsto_inf.1 this).2,
id            └───────────────┘    └─────────┘   └──┘
src      └───┘└───────────────┘└─┘ └─────────┘└─┘    └─┘
typ      └───┘└───────────────┘└─┘ └─────────┘└─┘└──┘└─┘
doc      └───┘                 └─┘            └─┘    └─┘
txt      └───┘                 └─┘            └─┘    └─┘
par      └───┘                 └─┘            └─┘    └─┘
pid      └───┘                 └─┘            └─┘    └┘
st   ──────────────────────────────────────────────────┘└─
120    apply tendsto_le_right h,
id           └──────────────┘ 
src    └────┘└──────────────┘
typ    └────┘└──────────────┘
doc    └────┘                
txt    └────┘                
par    └────┘                
pid                         
st   ─────────────────────────┘└─
121    refine tendsto_inf.2 ⟨_, tendsto_principal.2 ds⟩,
id            └─────────┘       └───────────────┘   └┘
src    └─────┘└─────────┘└─┘ └─┘└───────────────┘└─┘  
typ    └─────┘└─────────┘└─┘ └─┘└───────────────┘└─┘└┘
doc    └─────┘           └─┘ └─┘                 └─┘  
txt    └─────┘           └─┘ └─┘                 └─┘  
par    └─────┘           └─┘ └─┘                 └─┘  
pid                     └─┘ └─┘                 └─┘  
st   ─────────────────────────────────────────────────┘└─
122    simpa only [add_zero] using tendsto_const_nhds.add (tangent_cone_at.lim_zero at_top ctop clim)
id                 └──────┘        └────────────────────┘  └──────────────────────┘ └────┘ └──┘ └──┘
src    └──────────┘└──────┘└──────┘└────────────────────┘ └──────────────────────┘└────┘        └┘
typ    └──────────┘└──────┘└──────┘└────────────────────┘ └──────────────────────┘└────┘└──┘└──┘└┘
doc    └──────────┘        └──────┘                       └──────────────────────┘└────┘        └┘
txt    └──────────┘        └──────┘                                                             └┘
par    └──────────┘        └──────┘                                                             └┘
pid         └──┘└┘        └────┘                                                             
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘
123  end
st   └─┘
124  
125  /-- Tangent cone of `s` at `x` depends only on `nhds_within x s`. -/
126  lemma tangent_cone_congr (h : nhds_within x s = nhds_within x t) :
id                                 └─────────┘    └─────────┘  
src                                └─────────┘      └─────────┘
typ                                └─────────┘    └─────────┘  
doc                                └─────────┘       └─────────┘
127    tangent_cone_at 𝕜 s x = tangent_cone_at 𝕜 t x :=
id     └─────────────┘     └─────────────┘   
src    └─────────────┘        └─────────────┘
typ    └─────────────┘     └─────────────┘   
doc    └─────────────┘         └─────────────┘
128  subset.antisymm
id   └─────────────┘
src  └─────────────┘
typ  └─────────────┘
129    (tangent_cone_mono_nhds $ le_of_eq h)
id      └────────────────────┘   └──────┘ 
src     └────────────────────┘   └──────┘
typ     └────────────────────┘   └──────┘ 
130    (tangent_cone_mono_nhds $ le_of_eq h.symm)
id      └────────────────────┘   └──────┘ └───┘
src     └────────────────────┘   └──────┘  └───┘
typ     └────────────────────┘   └──────┘ └───┘
131  
132  /-- Intersecting with a neighborhood of the point does not change the tangent cone. -/
133  lemma tangent_cone_inter_nhds (ht : t ∈ 𝓝 x) :
id                                          
src                                         
typ                                         
doc                                          
134    tangent_cone_at 𝕜 (s ∩ t) x = tangent_cone_at 𝕜 s x :=
id     └─────────────┘         └─────────────┘   
src    └─────────────┘             └─────────────┘
typ    └─────────────┘         └─────────────┘   
doc    └─────────────┘               └─────────────┘
135  tangent_cone_congr (nhds_within_restrict' _ ht).symm
id   └────────────────┘  └───────────────────┘   └┘ └──┘
src  └────────────────┘  └───────────────────┘      └──┘
typ  └────────────────┘  └───────────────────┘   └┘ └──┘
doc  └────────────────┘
136  
137  /-- The tangent cone of a product contains the tangent cone of its left factor. -/
138  lemma subset_tangent_cone_prod_left {t : set F} {y : F} (ht : y ∈ closure t) :
id                                            └─┘                  └─────┘ 
src                                           └─┘                     └─────┘
typ                                           └─┘                  └─────┘ 
doc                                                                    └─────┘
139    set.prod (tangent_cone_at 𝕜 s x) {(0 : F)} ⊆ tangent_cone_at 𝕜 (set.prod s t) (x, y) :=
id     └──────┘  └─────────────┘              └─────────────┘   └──────┘      
src    └──────┘  └─────────────┘                  └─────────────┘    └──────┘      
typ    └──────┘  └─────────────┘              └─────────────┘   └──────┘      
doc    └──────┘  └─────────────┘                    └─────────────┘    └──────┘
140  begin
st   └─────
141    rintros ⟨v, w⟩ ⟨⟨c, d, hd, hc, hy⟩, hw⟩,
src    └─────────────────────────────────────┘
typ    └─────────────────────────────────────┘
doc    └─────────────────────────────────────┘
txt    └─────────────────────────────────────┘
par    └─────────────────────────────────────┘
pid           └──────────────────────────────┘
st   ────────────────────────────────────────┘└─
142    have : w = 0, by simpa using hw,
id                                └┘
src    └─────┘ └┘     └──────────┘
typ    └─────┘└┘     └──────────┘└┘
doc    └─────┘  └┘     └──────────┘
txt    └─────┘  └┘     └──────────┘
par    └─────┘  └┘     └──────────┘
pid    └───┘└┘            └────┘
st   ─────────────┘                   └─
143    rw this,
id        └──┘
src    └─┘
typ    └─┘└──┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────┘└─
144    have : ∀n, ∃d', y + d' ∈ t ∧ ∥c n • d'∥ ≤ ((1:ℝ)/2)^n,
id                                            
src    └─────┘  └┘           └┘ └┘
typ    └─────┘  └┘        └┘ └┘
doc    └─────┘   └┘                  └┘  └┘
txt    └─────┘   └┘                  └┘  └┘
par    └─────┘   └┘                  └┘  └┘
pid    └───┘└┘   └┘                  └┘  └┘
st   ──────────────────────────────────────────────────────┘└─
145    { assume n,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
146      have c_pos : 0 < 1 + ∥c n∥ :=
id                             
src      └─────────────┘└─┘     └───
typ      └─────────────┘└─┘   └───
doc      └─────────────┘ └─┘     └───
txt      └─────────────┘ └─┘     └───
par      └─────────────┘ └─┘     └───
pid      └────────┘└───┘ └─┘     └───
st   ──────────────────────────────────
147        add_pos_of_pos_of_nonneg zero_lt_one (norm_nonneg _),
id         └──────────────────────┘ └─────────┘  └─────────┘
src  ─────┘└──────────────────────┘└─────────┘ └─────────┘└─┘
typ  ─────┘└──────────────────────┘└─────────┘ └─────────┘└─┘
doc  ─────┘                                               └─┘
txt  ─────┘                                               └─┘
par  ─────┘                                               └─┘
pid  ─────┘                                               └─┘
st   ─────────────────────────────────────────────────────────┘└─
148      rcases metric.mem_closure_iff'.1 ht ((1 + ∥c n∥)⁻¹ * (1/2)^n) _ with ⟨z, z_pos, hz⟩,
id              └─────────────────────┘   └┘            └┘        
src      └─────┘└─────────────────────┘└─┘    └┘     └┘  └┘  └─────────────────────┘
typ      └─────┘└─────────────────────┘└─┘└┘  └┘    └┘  └┘ └─────────────────────┘
doc      └─────┘└─────────────────────┘└─┘    └┘          └┘  └─────────────────────┘
txt      └─────┘                       └─┘    └┘          └┘  └─────────────────────┘
par      └─────┘                       └─┘    └┘          └┘  └─────────────────────┘
pid                                   └─┘    └┘          └┘  └─────────────────────┘
st   ──────────────────────────────────────────────────────────────────────────────────────┘└─
149      refine ⟨z - y, _, _⟩,
id                 
src      └─────┘   └─────┘
typ      └─────┘ └─────┘
doc      └─────┘    └─────┘
txt      └─────┘    └─────┘
par      └─────┘    └─────┘
pid                └─────┘
st   ───────────────────────┘└─
150      { convert z_pos, abel },
id                 └───┘
src        └──────┘       └───┘
typ        └──────┘└───┘  └───┘
doc        └──────┘       └───┘
txt        └──────┘       └───┘
par        └──────┘       └───┘
pid                          
st   ─────┘└───────────┘└─────┘└┘
151      { rw [norm_smul, ← dist_eq_norm, dist_comm],
id             └───────┘    └──────────┘  └───────┘
src        └──┘└───────┘└──┘└──────────┘└┘└───────┘
typ        └──┘└───────┘└──┘└──────────┘└┘└───────┘
doc        └──┘         └──┘            └┘         
txt        └──┘         └──┘            └┘         
par        └──┘         └──┘            └┘         
pid          └┘         └──┘            └┘         
st   ─────┘└───────────┘└──────────────┘└─────────┘└──
152        calc ∥c n∥ * dist y z ≤ (1 + ∥c n∥) * ((1 + ∥c n∥)⁻¹ * (1/2)^n) :
id         └──┘         └──┘                          
src        └──┘         └──┘
typ        └──┘         └──┘                          
doc        └──┘
st   ────────────────────────────────────────────────────────────────────────
153        begin
st   ─────┘└─────
154          apply mul_le_mul _ (le_of_lt hz) dist_nonneg (le_of_lt c_pos),
id                 └────────┘             └┘  └─────────┘  └──────┘ └───┘
src          └────┘└────────┘└─┘           └┘└─────────┘ └──────┘     
typ          └────┘└────────┘└─┘         └┘└┘└─────────┘ └──────┘└───┘
doc          └────┘          └─┘           └┘                         
txt          └────┘          └─┘           └┘                         
par          └────┘          └─┘           └┘                         
pid                         └─┘           └┘                         
st   ────────────────────────────────────────────────────────────────────┘└─
155          simp only [zero_le_one, le_add_iff_nonneg_left]
id                      └─────────┘  └────────────────────┘
src          └─────────┘└─────────┘└┘└────────────────────┘└─
typ          └─────────┘└─────────┘└┘└────────────────────┘└─
doc          └─────────┘           └┘                      └─
txt          └─────────┘           └┘                      └─
par          └─────────┘           └┘                      └─
pid              └──┘└┘           └┘                      
st   ────────────────────────────────────────────────────────
156        end
src  ─────┘
typ  ─────┘
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘└─┘
157        ... = (1/2)^n :
id                     
typ                    
st   ──────────────────────
158        begin
st   ─────┘└─────
159          rw [← mul_assoc, mul_inv_cancel, one_mul],
id                 └───────┘  └────────────┘  └─────┘
src          └────┘└───────┘└┘└────────────┘└┘└─────┘
typ          └────┘└───────┘└┘└────────────┘└┘└─────┘
doc          └────┘         └┘              └┘       
txt          └────┘         └┘              └┘       
par          └────┘         └┘              └┘       
pid            └──┘         └┘              └┘       
st   ──────────────────────┘└──────────────┘└───────┘└──
160          exact ne_of_gt c_pos
id                 └──────┘ └───┘
src          └────┘└──────┘     
typ          └────┘└──────┘└───┘
doc          └────┘             
txt          └────┘             
par          └────┘             
pid                            
st   ─────────────────────────────
161        end },
src  ─────┘
typ  ─────┘
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘└────┘
162      { apply mul_pos (inv_pos c_pos) (pow_pos _ _),
id               └─────┘  └─────┘ └───┘   └─────┘
src        └────┘└─────┘ └─────┘     └┘ └─────┘└───┘
typ        └────┘└─────┘ └─────┘└───┘└┘ └─────┘└───┘
doc        └────┘                    └┘        └───┘
txt        └────┘                    └┘        └───┘
par        └────┘                    └┘        └───┘
pid                                 └┘        └───┘
st   ────────────────────────────────────────────────┘└─
163        norm_num } },
src        └───────┘
typ        └───────┘
doc        └───────┘
txt        └───────┘
par        └───────┘
pid                
st   ──────────────┘└──┘
164    choose d' hd' using this,
id                         └──┘
src    └──────────────────┘
typ    └──────────────────┘└──┘
doc    └──────────────────┘
txt    └──────────────────┘
par    └──────────────────┘
pid          └─┘└──┘└─────┘
st   ─────────────────────────┘└─
165    refine ⟨c, λn, (d n, d' n), _, hc, _⟩,
id                        └┘        └┘
src    └─────┘  └┘ └─┘   └┘   └────┘  └──┘
typ    └─────┘ └┘ └─┘  └┘└┘ └────┘└┘└──┘
doc    └─────┘  └┘ └─┘   └┘   └────┘  └──┘
txt    └─────┘  └┘ └─┘   └┘   └────┘  └──┘
par    └─────┘  └┘ └─┘   └┘   └────┘  └──┘
pid            └┘ └─┘   └┘   └────┘  └──┘
st   ──────────────────────────────────────┘└─
166    show ∀ᶠ n in at_top, (x, y) + (d n, d' n) ∈ set.prod s t,
id          └┘   └┘ └────┘            └┘      └──────┘  
src    └───┘└┘└─┘└┘└────┘  └┘ └┘   └┘   └┘ └──────┘ 
typ    └───┘└┘└─┘└┘└────┘ └┘└┘  └┘└┘ └┘ └──────┘
doc    └───┘└┘└─┘└┘└────┘  └┘ └┘    └┘   └┘ └──────┘ 
txt    └───┘  └─┘           └┘ └┘    └┘   └┘          
par    └───┘  └─┘           └┘ └┘    └┘   └┘          
pid    └───┘  └─┘           └┘ └┘    └┘   └┘          
st   ─────────────────────────────────────────────────────────┘└─
167    { apply filter.mem_sets_of_superset hd,
id             └─────────────────────────┘ └┘
src      └────┘└─────────────────────────┘
typ      └────┘└─────────────────────────┘└┘
doc      └────┘                           
txt      └────┘                           
par      └────┘                           
pid                                      
st   ───┘└──────────────────────────────────┘└─
168      assume n hn,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ──────────────┘└─
169      simp at hn,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid          └───┘
st   ─────────────┘└─
170      simp [hn, (hd' n).1] },
id             └┘   └─┘ 
src      └────┘  └┘     └───┘
typ      └────┘└┘└┘ └─┘└───┘
doc      └────┘  └┘     └───┘
txt      └────┘  └┘     └───┘
par      └────┘  └┘     └───┘
pid            └┘     └──┘
st   ────────────────────────┘└┘
171    { apply tendsto_prod_mk_nhds hy,
id             └──────────────────┘ └┘
src      └────┘└──────────────────┘
typ      └────┘└──────────────────┘└┘
doc      └────┘                    
txt      └────┘                    
par      └────┘                    
pid                               
st   ────────────────────────────────┘└─
172      change tendsto (λ (n : ℕ), c n • d' n) at_top (𝓝 0),
id              └─────┘                  └┘    └────┘  
src      └─────┘└─────┘  └────┘ └─┘      └┘└────┘ └─┘
typ      └─────┘└─────┘  └────┘ └─┘  └┘ └┘└────┘ └─┘
doc      └─────┘└─────┘  └────┘ └─┘      └┘└────┘ └─┘
txt      └─────┘         └────┘ └─┘      └┘        └─┘
par      └─────┘         └────┘ └─┘      └┘        └─┘
pid                     └────┘ └─┘      └┘        └─┘
st   ──────────────────────────────────────────────────────┘└─
173      rw tendsto_zero_iff_norm_tendsto_zero,
id          └────────────────────────────────┘
src      └─┘└────────────────────────────────┘
typ      └─┘└────────────────────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ────────────────────────────────────────┘└─
174      refine squeeze_zero (λn, norm_nonneg _) (λn, (hd' n).2) _,
id              └──────────┘      └─────────┘          └─┘
src      └─────┘└──────────┘  └─┘└─────────┘└──┘  └─┘     └────┘
typ      └─────┘└──────────┘  └─┘└─────────┘└──┘  └─┘ └─┘ └────┘
doc      └─────┘              └─┘           └──┘  └─┘     └────┘
txt      └─────┘              └─┘           └──┘  └─┘     └────┘
par      └─────┘              └─┘           └──┘  └─┘     └────┘
pid                          └─┘           └──┘  └─┘     └────┘
st   ────────────────────────────────────────────────────────────┘└─
175      apply tendsto_pow_at_top_nhds_0_of_lt_1; norm_num }
id             └───────────────────────────────┘
src      └────┘└───────────────────────────────┘  └───────┘
typ      └────┘└───────────────────────────────┘  └───────┘
doc      └────┘                                   └───────┘
txt      └────┘                                   └───────┘
par      └────┘                                   └───────┘
pid                                                      
st   ─────────────────────────────────────────────────────┘└─
176  end
st   ──┘
177  
178  /-- The tangent cone of a product contains the tangent cone of its right factor. -/
179  lemma subset_tangent_cone_prod_right {t : set F} {y : F}
id                                             └─┘        
src                                            └─┘
typ                                            └─┘        
180    (hs : x ∈ closure s) :
id             └─────┘ 
src             └─────┘
typ            └─────┘ 
doc              └─────┘
181    set.prod {(0 : E)} (tangent_cone_at 𝕜 t y) ⊆ tangent_cone_at 𝕜 (set.prod s t) (x, y) :=
id     └──────┘          └─────────────┘      └─────────────┘   └──────┘      
src    └──────┘           └─────────────┘         └─────────────┘    └──────┘      
typ    └──────┘          └─────────────┘      └─────────────┘   └──────┘      
doc    └──────┘            └─────────────┘          └─────────────┘    └──────┘
182  begin
st   └─────
183    rintros ⟨v, w⟩ ⟨hv, ⟨c, d, hd, hc, hy⟩⟩,
src    └─────────────────────────────────────┘
typ    └─────────────────────────────────────┘
doc    └─────────────────────────────────────┘
txt    └─────────────────────────────────────┘
par    └─────────────────────────────────────┘
pid           └──────────────────────────────┘
st   ────────────────────────────────────────┘└─
184    have : v = 0, by simpa using hv,
id                                └┘
src    └─────┘ └┘     └──────────┘
typ    └─────┘└┘     └──────────┘└┘
doc    └─────┘  └┘     └──────────┘
txt    └─────┘  └┘     └──────────┘
par    └─────┘  └┘     └──────────┘
pid    └───┘└┘            └────┘
st   ─────────────┘                   └─
185    rw this,
id        └──┘
src    └─┘
typ    └─┘└──┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────┘└─
186    have : ∀n, ∃d', x + d' ∈ s ∧ ∥c n • d'∥ ≤ ((1:ℝ)/2)^n,
id                                            
src    └─────┘  └┘           └┘ └┘
typ    └─────┘  └┘        └┘ └┘
doc    └─────┘   └┘                  └┘  └┘
txt    └─────┘   └┘                  └┘  └┘
par    └─────┘   └┘                  └┘  └┘
pid    └───┘└┘   └┘                  └┘  └┘
st   ──────────────────────────────────────────────────────┘└─
187    { assume n,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
188      have c_pos : 0 < 1 + ∥c n∥ :=
id                             
src      └─────────────┘└─┘     └───
typ      └─────────────┘└─┘   └───
doc      └─────────────┘ └─┘     └───
txt      └─────────────┘ └─┘     └───
par      └─────────────┘ └─┘     └───
pid      └────────┘└───┘ └─┘     └───
st   ──────────────────────────────────
189        add_pos_of_pos_of_nonneg zero_lt_one (norm_nonneg _),
id         └──────────────────────┘ └─────────┘  └─────────┘
src  ─────┘└──────────────────────┘└─────────┘ └─────────┘└─┘
typ  ─────┘└──────────────────────┘└─────────┘ └─────────┘└─┘
doc  ─────┘                                               └─┘
txt  ─────┘                                               └─┘
par  ─────┘                                               └─┘
pid  ─────┘                                               └─┘
st   ─────────────────────────────────────────────────────────┘└─
190      rcases metric.mem_closure_iff'.1 hs ((1 + ∥c n∥)⁻¹ * (1/2)^n) _ with ⟨z, z_pos, hz⟩,
id              └─────────────────────┘   └┘            └┘        
src      └─────┘└─────────────────────┘└─┘    └┘     └┘  └┘  └─────────────────────┘
typ      └─────┘└─────────────────────┘└─┘└┘  └┘    └┘  └┘ └─────────────────────┘
doc      └─────┘└─────────────────────┘└─┘    └┘          └┘  └─────────────────────┘
txt      └─────┘                       └─┘    └┘          └┘  └─────────────────────┘
par      └─────┘                       └─┘    └┘          └┘  └─────────────────────┘
pid                                   └─┘    └┘          └┘  └─────────────────────┘
st   ──────────────────────────────────────────────────────────────────────────────────────┘└─
191      refine ⟨z - x, _, _⟩,
id                 
src      └─────┘   └─────┘
typ      └─────┘ └─────┘
doc      └─────┘    └─────┘
txt      └─────┘    └─────┘
par      └─────┘    └─────┘
pid                └─────┘
st   ───────────────────────┘└─
192      { convert z_pos, abel },
id                 └───┘
src        └──────┘       └───┘
typ        └──────┘└───┘  └───┘
doc        └──────┘       └───┘
txt        └──────┘       └───┘
par        └──────┘       └───┘
pid                          
st   ─────┘└───────────┘└─────┘└┘
193      { rw [norm_smul, ← dist_eq_norm, dist_comm],
id             └───────┘    └──────────┘  └───────┘
src        └──┘└───────┘└──┘└──────────┘└┘└───────┘
typ        └──┘└───────┘└──┘└──────────┘└┘└───────┘
doc        └──┘         └──┘            └┘         
txt        └──┘         └──┘            └┘         
par        └──┘         └──┘            └┘         
pid          └┘         └──┘            └┘         
st   ─────┘└───────────┘└──────────────┘└─────────┘└──
194        calc ∥c n∥ * dist x z ≤ (1 + ∥c n∥) * ((1 + ∥c n∥)⁻¹ * (1/2)^n) :
id         └──┘         └──┘                          
src        └──┘         └──┘
typ        └──┘         └──┘                          
doc        └──┘
st   ────────────────────────────────────────────────────────────────────────
195        begin
st   ─────┘└─────
196          apply mul_le_mul _ (le_of_lt hz) dist_nonneg (le_of_lt c_pos),
id                 └────────┘             └┘  └─────────┘  └──────┘ └───┘
src          └────┘└────────┘└─┘           └┘└─────────┘ └──────┘     
typ          └────┘└────────┘└─┘         └┘└┘└─────────┘ └──────┘└───┘
doc          └────┘          └─┘           └┘                         
txt          └────┘          └─┘           └┘                         
par          └────┘          └─┘           └┘                         
pid                         └─┘           └┘                         
st   ────────────────────────────────────────────────────────────────────┘└─
197          simp only [zero_le_one, le_add_iff_nonneg_left]
id                      └─────────┘  └────────────────────┘
src          └─────────┘└─────────┘└┘└────────────────────┘└─
typ          └─────────┘└─────────┘└┘└────────────────────┘└─
doc          └─────────┘           └┘                      └─
txt          └─────────┘           └┘                      └─
par          └─────────┘           └┘                      └─
pid              └──┘└┘           └┘                      
st   ────────────────────────────────────────────────────────
198        end
src  ─────┘
typ  ─────┘
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘└─┘
199        ... = (1/2)^n :
id                     
typ                    
st   ──────────────────────
200        begin
st   ─────┘└─────
201          rw [← mul_assoc, mul_inv_cancel, one_mul],
id                 └───────┘  └────────────┘  └─────┘
src          └────┘└───────┘└┘└────────────┘└┘└─────┘
typ          └────┘└───────┘└┘└────────────┘└┘└─────┘
doc          └────┘         └┘              └┘       
txt          └────┘         └┘              └┘       
par          └────┘         └┘              └┘       
pid            └──┘         └┘              └┘       
st   ──────────────────────┘└──────────────┘└───────┘└──
202          exact ne_of_gt c_pos
id                 └──────┘ └───┘
src          └────┘└──────┘     
typ          └────┘└──────┘└───┘
doc          └────┘             
txt          └────┘             
par          └────┘             
pid                            
st   ─────────────────────────────
203        end },
src  ─────┘
typ  ─────┘
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘└────┘
204      { apply mul_pos (inv_pos c_pos) (pow_pos _ _),
id               └─────┘  └─────┘ └───┘   └─────┘
src        └────┘└─────┘ └─────┘     └┘ └─────┘└───┘
typ        └────┘└─────┘ └─────┘└───┘└┘ └─────┘└───┘
doc        └────┘                    └┘        └───┘
txt        └────┘                    └┘        └───┘
par        └────┘                    └┘        └───┘
pid                                 └┘        └───┘
st   ────────────────────────────────────────────────┘└─
205        norm_num } },
src        └───────┘
typ        └───────┘
doc        └───────┘
txt        └───────┘
par        └───────┘
pid                
st   ──────────────┘└──┘
206    choose d' hd' using this,
id                         └──┘
src    └──────────────────┘
typ    └──────────────────┘└──┘
doc    └──────────────────┘
txt    └──────────────────┘
par    └──────────────────┘
pid          └─┘└──┘└─────┘
st   ─────────────────────────┘└─
207    refine ⟨c, λn, (d' n, d n), _, hc, _⟩,
id                    └┘            └┘
src    └─────┘  └┘ └─┘    └┘  └────┘  └──┘
typ    └─────┘ └┘ └─┘ └┘ └┘ └────┘└┘└──┘
doc    └─────┘  └┘ └─┘    └┘  └────┘  └──┘
txt    └─────┘  └┘ └─┘    └┘  └────┘  └──┘
par    └─────┘  └┘ └─┘    └┘  └────┘  └──┘
pid            └┘ └─┘    └┘  └────┘  └──┘
st   ──────────────────────────────────────┘└─
208    show ∀ᶠ n in at_top, (x, y) + (d' n, d n) ∈ set.prod s t,
id          └┘   └┘ └────┘        └┘          └──────┘  
src    └───┘└┘└─┘└┘└────┘  └┘ └┘    └┘  └┘ └──────┘ 
typ    └───┘└┘└─┘└┘└────┘ └┘└┘ └┘ └┘ └┘ └──────┘
doc    └───┘└┘└─┘└┘└────┘  └┘ └┘     └┘  └┘ └──────┘ 
txt    └───┘  └─┘           └┘ └┘     └┘  └┘          
par    └───┘  └─┘           └┘ └┘     └┘  └┘          
pid    └───┘  └─┘           └┘ └┘     └┘  └┘          
st   ─────────────────────────────────────────────────────────┘└─
209    { apply filter.mem_sets_of_superset hd,
id             └─────────────────────────┘ └┘
src      └────┘└─────────────────────────┘
typ      └────┘└─────────────────────────┘└┘
doc      └────┘                           
txt      └────┘                           
par      └────┘                           
pid                                      
st   ───┘└──────────────────────────────────┘└─
210      assume n hn,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ──────────────┘└─
211      simp at hn,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid          └───┘
st   ─────────────┘└─
212      simp [hn, (hd' n).1] },
id             └┘   └─┘ 
src      └────┘  └┘     └───┘
typ      └────┘└┘└┘ └─┘└───┘
doc      └────┘  └┘     └───┘
txt      └────┘  └┘     └───┘
par      └────┘  └┘     └───┘
pid            └┘     └──┘
st   ────────────────────────┘└┘
213    { apply tendsto_prod_mk_nhds _ hy,
id             └──────────────────┘   └┘
src      └────┘└──────────────────┘└─┘
typ      └────┘└──────────────────┘└─┘└┘
doc      └────┘                    └─┘
txt      └────┘                    └─┘
par      └────┘                    └─┘
pid                               └─┘
st   ──────────────────────────────────┘└─
214      change tendsto (λ (n : ℕ), c n • d' n) at_top (𝓝 0),
id              └─────┘                  └┘    └────┘  
src      └─────┘└─────┘  └────┘ └─┘      └┘└────┘ └─┘
typ      └─────┘└─────┘  └────┘ └─┘  └┘ └┘└────┘ └─┘
doc      └─────┘└─────┘  └────┘ └─┘      └┘└────┘ └─┘
txt      └─────┘         └────┘ └─┘      └┘        └─┘
par      └─────┘         └────┘ └─┘      └┘        └─┘
pid                     └────┘ └─┘      └┘        └─┘
st   ──────────────────────────────────────────────────────┘└─
215      rw tendsto_zero_iff_norm_tendsto_zero,
id          └────────────────────────────────┘
src      └─┘└────────────────────────────────┘
typ      └─┘└────────────────────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ────────────────────────────────────────┘└─
216      refine squeeze_zero (λn, norm_nonneg _) (λn, (hd' n).2) _,
id              └──────────┘      └─────────┘          └─┘
src      └─────┘└──────────┘  └─┘└─────────┘└──┘  └─┘     └────┘
typ      └─────┘└──────────┘  └─┘└─────────┘└──┘  └─┘ └─┘ └────┘
doc      └─────┘              └─┘           └──┘  └─┘     └────┘
txt      └─────┘              └─┘           └──┘  └─┘     └────┘
par      └─────┘              └─┘           └──┘  └─┘     └────┘
pid                          └─┘           └──┘  └─┘     └────┘
st   ────────────────────────────────────────────────────────────┘└─
217      apply tendsto_pow_at_top_nhds_0_of_lt_1; norm_num }
id             └───────────────────────────────┘
src      └────┘└───────────────────────────────┘  └───────┘
typ      └────┘└───────────────────────────────┘  └───────┘
doc      └────┘                                   └───────┘
txt      └────┘                                   └───────┘
par      └────┘                                   └───────┘
pid                                                      
st   ─────────────────────────────────────────────────────┘└─
218  end
st   ──┘
219  
220  /-- If a subset of a real vector space contains a segment, then the direction of this
221  segment belongs to the tangent cone at its endpoints. -/
222  lemma mem_tangent_cone_of_segment_subset {s : set G} {x y : G} (h : segment x y ⊆ s) :
id                                                 └─┘                 └─────┘    
src                                                └─┘                   └─────┘     
typ                                                └─┘                 └─────┘    
doc                                                                      └─────┘
223    y - x ∈ tangent_cone_at ℝ s x :=
id         └─────────────┘   
src          └─────────────┘ 
typ        └─────────────┘   
doc            └─────────────┘
224  begin
st   └─────
225    let w : ℝ := 2,
id             
src    └──────┘└───┘
typ    └──────┘└───┘
doc    └──────┘ └───┘
txt    └──────┘ └───┘
par    └──────┘ └───┘
pid    └───┘└─┘ └──┘
st   ───────────────┘└─
226    let c := λn:ℕ, (2:ℝ)^n,
id                         
src    └───────┘ └┘ └┘ └┘ 
typ    └───────┘ └┘ └┘ └┘ 
doc    └───────┘ └┘ └┘ └┘ 
txt    └───────┘ └┘ └┘ └┘ 
par    └───────┘ └┘ └┘ └┘ 
pid    └───┘└─┘ └┘ └┘ └┘ 
st   ───────────────────────┘└─
227    let d := λn:ℕ, (c n)⁻¹ • (y-x),
id                        └┘   
src    └───────┘ └┘ └┘   └┘   
typ    └───────┘ └┘ └┘  └┘ 
doc    └───────┘ └┘ └┘          
txt    └───────┘ └┘ └┘          
par    └───────┘ └┘ └┘          
pid    └───┘└─┘ └┘ └┘          
st   ───────────────────────────────┘└─
228    refine ⟨c, d, filter.univ_mem_sets' (λn, h _), _, _⟩,
id                 └───────────────────┘      
src    └─────┘  └┘ └┘└───────────────────┘  └─┘ └────────┘
typ    └─────┘ └┘└┘└───────────────────┘  └─┘└────────┘
doc    └─────┘  └┘ └┘                       └─┘ └────────┘
txt    └─────┘  └┘ └┘                       └─┘ └────────┘
par    └─────┘  └┘ └┘                       └─┘ └────────┘
pid            └┘ └┘                       └─┘ └────────┘
st   ─────────────────────────────────────────────────────┘└─
229    show x + d n ∈ segment x y,
id                └─────┘  
src    └───┘   └─────┘ 
typ    └───┘ └─────┘
doc    └───┘     └─────┘ 
txt    └───┘             
par    └───┘             
pid    └───┘             
st   ──────────────────────────────
230    { rw segment_eq_image,
id          └──────────────┘
src      └─┘└──────────────┘
typ      └─┘└──────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───┘└─────────────────┘└─
231      refine ⟨(c n)⁻¹, ⟨_, _⟩, _⟩,
id                 
src      └─────┘      └┘ └───────┘
typ      └─────┘    └┘ └───────┘
doc      └─────┘      └┘ └───────┘
txt      └─────┘      └┘ └───────┘
par      └─────┘      └┘ └───────┘
pid                  └┘ └───────┘
st   ──────────────────────────────┘└─
232      { rw inv_nonneg, apply pow_nonneg, norm_num },
id            └────────┘        └────────┘
src        └─┘└────────┘  └────┘└────────┘  └───────┘
typ        └─┘└────────┘  └────┘└────────┘  └───────┘
doc        └─┘            └────┘            └───────┘
txt        └─┘            └────┘            └───────┘
par        └─┘            └────┘            └───────┘
pid                                               
st   ─────┘└───────────┘└────────────────┘└─────────┘└┘
233      { apply inv_le_one, apply one_le_pow_of_one_le, norm_num },
id               └────────┘        └──────────────────┘
src        └────┘└────────┘  └────┘└──────────────────┘  └───────┘
typ        └────┘└────────┘  └────┘└──────────────────┘  └───────┘
doc        └────┘            └────┘                      └───────┘
txt        └────┘            └────┘                      └───────┘
par        └────┘            └────┘                      └───────┘
pid                                                            
st   ─────┘└──────────────┘└──────────────────────────┘└─────────┘└┘
234      { simp only [d, sub_smul, smul_sub, one_smul], abel } },
id                      └──────┘  └──────┘  └──────┘
src        └─────────┘ └┘└──────┘└┘└──────┘└┘└──────┘  └───┘
typ        └─────────┘└┘└──────┘└┘└──────┘└┘└──────┘  └───┘
doc        └─────────┘ └┘        └┘        └┘          └───┘
txt        └─────────┘ └┘        └┘        └┘          └───┘
par        └─────────┘ └┘        └┘        └┘          └───┘
pid            └──┘└┘ └┘        └┘        └┘              
st   ────────────────────────────────────────────────┘└─────┘└──┘
235    show filter.tendsto (λ (n : ℕ), ∥c n∥) filter.at_top filter.at_top,
id          └────────────┘                               └───────────┘
src    └───┘└────────────┘  └────┘ └─┘  └┘             └───────────┘
typ    └───┘└────────────┘  └────┘ └─┘ └┘             └───────────┘
doc    └───┘└────────────┘  └────┘ └─┘    └┘             └───────────┘
txt    └───┘                └────┘ └─┘    └┘             
par    └───┘                └────┘ └─┘    └┘             
pid    └───┘                └────┘ └─┘    └┘             
st   ───────────────────────────────────────────────────────────────────┘└─
236    { have : (λ (n : ℕ), ∥c n∥) = c,
id                                  
src      └─────┘  └────┘ └─┘    └┘
typ      └─────┘  └────┘ └─┘    └┘
doc      └─────┘  └────┘ └─┘    └┘ 
txt      └─────┘  └────┘ └─┘    └┘ 
par      └─────┘  └────┘ └─┘    └┘ 
pid      └───┘└┘  └────┘ └─┘    └┘ 
st   ───┘└───────────────────────────┘
237        by { ext n, exact abs_of_nonneg (pow_nonneg (by norm_num) _) },
id                           └───────────┘  └────────┘
src             └───┘  └────┘└───────────┘ └────────┘   └──────┘└───┘
typ             └───┘  └────┘└───────────┘ └────────┘   └──────┘└───┘
doc             └───┘  └────┘                           └──────┘└───┘
txt             └───┘  └────┘                           └──────┘└───┘
par             └───┘  └────┘                           └──────┘└───┘
pid                └┘                                  └───────────┘
st            └────┘└───────────────────────────────────┘└───────┘└───┘└┘
238      rw this,
id          └──┘
src      └─┘
typ      └─┘└──┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ──────────┘└─
239      exact tendsto_pow_at_top_at_top_of_gt_1 (by norm_num) },
id             └───────────────────────────────┘
src      └────┘└───────────────────────────────┘   └──────┘└┘
typ      └────┘└───────────────────────────────┘   └──────┘└┘
doc      └────┘                                    └──────┘└┘
txt      └────┘                                    └──────┘└┘
par      └────┘                                    └──────┘└┘
pid                                               └────────┘
st   ──────────────────────────────────────────────┘└───────┘└┘└┘
240    show filter.tendsto (λ (n : ℕ), c n • d n) filter.at_top (𝓝 (y - x)),
id          └────────────┘                      └───────────┘       
src    └───┘└────────────┘  └────┘ └─┘     └┘└───────────┘     └┘
typ    └───┘└────────────┘  └────┘ └─┘   └┘└───────────┘   └┘
doc    └───┘└────────────┘  └────┘ └─┘     └┘└───────────┘     └┘
txt    └───┘                └────┘ └─┘     └┘                   └┘
par    └───┘                └────┘ └─┘     └┘                   └┘
pid    └───┘                └────┘ └─┘     └┘                   └┘
st   ─────────────────────────────────────────────────────────────────────┘└─
241    { have : (λ (n : ℕ), c n • d n) = (λn, y - x),
id                                             
src      └─────┘  └────┘ └─┘     └┘   └─┘   
typ      └─────┘  └────┘ └─┘   └┘   └─┘ 
doc      └─────┘  └────┘ └─┘     └┘   └─┘   
txt      └─────┘  └────┘ └─┘     └┘   └─┘   
par      └─────┘  └────┘ └─┘     └┘   └─┘   
pid      └───┘└┘  └────┘ └─┘     └┘   └─┘   
st   ──────────────────────────────────────────────┘└─
242      { ext n,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid           └┘
st   ─────┘└───┘└─
243        simp only [d, smul_smul],
id                      └───────┘
src        └─────────┘ └┘└───────┘
typ        └─────────┘└┘└───────┘
doc        └─────────┘ └┘         
txt        └─────────┘ └┘         
par        └─────────┘ └┘         
pid            └──┘└┘ └┘         
st   ─────────────────────────────┘└─
244        rw [mul_inv_cancel, one_smul],
id             └────────────┘  └──────┘
src        └──┘└────────────┘└┘└──────┘
typ        └──┘└────────────┘└┘└──────┘
doc        └──┘              └┘        
txt        └──┘              └┘        
par        └──┘              └┘        
pid          └┘              └┘        
st   ───────────────────────┘└────────┘└──
245        exact pow_ne_zero _ (by norm_num) },
id               └─────────┘
src        └────┘└─────────┘└─┘   └──────┘└┘
typ        └────┘└─────────┘└─┘   └──────┘└┘
doc        └────┘           └─┘   └──────┘└┘
txt        └────┘           └─┘   └──────┘└┘
par        └────┘           └─┘   └──────┘└┘
pid                        └─┘   └────────┘
st   ────────────────────────────┘└───────┘└┘└┘
246      rw this,
id          └──┘
src      └─┘
typ      └─┘└──┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ──────────┘└─
247      apply tendsto_const_nhds }
id             └────────────────┘
src      └────┘└────────────────┘
typ      └────┘└────────────────┘
doc      └────┘                  
txt      └────┘                  
par      └────┘                  
pid                             
st   ────────────────────────────┘└─
248  end
st   ──┘
249  
250  end tangent_cone
251  
252  section unique_diff
253  /- This section is devoted to properties of the predicates `unique_diff_within_at` and
254  `unique_diff_on`. -/
255  
256  lemma unique_diff_within_at_univ : unique_diff_within_at 𝕜 univ x :=
id                                      └───────────────────┘  └──┘ 
src                                     └───────────────────┘   └──┘
typ                                     └───────────────────┘  └──┘ 
doc                                     └───────────────────┘
257  by { rw [unique_diff_within_at, tangent_cone_univ], simp }
id            └───────────────────┘  └───────────────┘
src       └──┘└───────────────────┘└┘└───────────────┘  └───┘
typ       └──┘└───────────────────┘└┘└───────────────┘  └───┘
doc       └──┘└───────────────────┘└┘                   └───┘
txt       └──┘                     └┘                   └───┘
par       └──┘                     └┘                   └───┘
pid         └┘                     └┘                       
st     └──────────────────────────┘└─────────────────┘└──────┘└┘
258  
259  lemma unique_diff_on_univ : unique_diff_on 𝕜 (univ : set E) :=
id                               └────────────┘   └──┘   └─┘ 
src                              └────────────┘    └──┘   └─┘
typ                              └────────────┘   └──┘   └─┘ 
doc                              └────────────┘
260  λx hx, unique_diff_within_at_univ
id     └┘  └────────────────────────┘
src         └────────────────────────┘
typ    └┘  └────────────────────────┘
261  
262  lemma unique_diff_within_at.mono_nhds (h : unique_diff_within_at 𝕜 s x)
id                                              └───────────────────┘   
src                                             └───────────────────┘
typ                                             └───────────────────┘   
doc                                             └───────────────────┘
263    (st : nhds_within x s ≤ nhds_within x t) :
id           └─────────┘    └─────────┘  
src          └─────────┘      └─────────┘
typ          └─────────┘    └─────────┘  
doc          └─────────┘       └─────────┘
264    unique_diff_within_at 𝕜 t x :=
id     └───────────────────┘   
src    └───────────────────┘
typ    └───────────────────┘   
doc    └───────────────────┘
265  begin
st   └─────
266    unfold unique_diff_within_at at *,
src    └───────────────────────────────┘
typ    └───────────────────────────────┘
doc    └───────────────────────────────┘
txt    └───────────────────────────────┘
par    └───────────────────────────────┘
pid          └────────────────────┘└───┘
st   ──────────────────────────────────┘└─
267    rw [← univ_subset_iff, ← h.1],
id           └─────────────┘    
src    └────┘└─────────────┘└──┘ └─┘
typ    └────┘└─────────────┘└──┘└─┘
doc    └────┘               └──┘ └─┘
txt    └────┘               └──┘ └─┘
par    └────┘               └──┘ └─┘
pid      └──┘               └──┘ └─┘
st   ──────────────────────┘└───┘└────
268    rw [mem_closure_iff_nhds_within_ne_bot] at h ⊢,
id         └────────────────────────────────┘
src    └──┘└────────────────────────────────┘└──────┘
typ    └──┘└────────────────────────────────┘└──────┘
doc    └──┘                                  └──────┘
txt    └──┘                                  └──────┘
par    └──┘                                  └──────┘
pid      └┘                                  └─────┘
st   ───────────────────────────────────────┘└─────┘└─
269    exact ⟨closure_mono (submodule.span_mono (tangent_cone_mono_nhds st)),
id            └──────────┘  └─────────────────┘  └────────────────────┘
src    └────┘ └──────────┘ └─────────────────┘ └────────────────────┘  └───
typ    └────┘ └──────────┘ └─────────────────┘ └────────────────────┘  └───
doc    └────┘                                                          └───
txt    └────┘                                                          └───
par    └────┘                                                          └───
pid                                                                   └───
st   ─────────────────────────────────────────────────────────────────────────
270      lattice.ne_bot_of_le_ne_bot h.2 st⟩
id       └─────────────────────────┘    └┘
src  ───┘└─────────────────────────┘ └─┘  └┘
typ  ───┘└─────────────────────────┘└─┘└┘└┘
doc  ───┘                            └─┘  └┘
txt  ───┘                            └─┘  └┘
par  ───┘                            └─┘  └┘
pid  ───┘                            └─┘  
st   ───────────────────────────────────────┘
271  end
st   └─┘
272  
273  lemma unique_diff_within_at.mono (h : unique_diff_within_at 𝕜 s x) (st : s ⊆ t) :
id                                         └───────────────────┘             
src                                        └───────────────────┘                
typ                                        └───────────────────┘             
doc                                        └───────────────────┘
274    unique_diff_within_at 𝕜 t x :=
id     └───────────────────┘   
src    └───────────────────┘
typ    └───────────────────┘   
doc    └───────────────────┘
275  h.mono_nhds $ nhds_within_mono _ st
id   └────────┘   └──────────────┘   └┘
src   └────────┘   └──────────────┘
typ  └────────┘   └──────────────┘   └┘
276  
277  lemma unique_diff_within_at_congr (st : nhds_within x s = nhds_within x t) :
id                                           └─────────┘    └─────────┘  
src                                          └─────────┘      └─────────┘
typ                                          └─────────┘    └─────────┘  
doc                                          └─────────┘       └─────────┘
278    unique_diff_within_at 𝕜 s x ↔ unique_diff_within_at 𝕜 t x :=
id     └───────────────────┘     └───────────────────┘   
src    └───────────────────┘        └───────────────────┘
typ    └───────────────────┘     └───────────────────┘   
doc    └───────────────────┘         └───────────────────┘
279  ⟨λ h, h.mono_nhds $ le_of_eq st, λ h, h.mono_nhds $ le_of_eq st.symm⟩
id        └────────┘   └──────┘ └┘      └────────┘   └──────┘ └┘└───┘
src         └────────┘   └──────┘           └────────┘   └──────┘   └───┘
typ       └────────┘   └──────┘ └┘      └────────┘   └──────┘ └┘└───┘
280  
281  lemma unique_diff_within_at_inter (ht : t ∈ 𝓝 x) :
id                                              
src                                             
typ                                             
doc                                              
282    unique_diff_within_at 𝕜 (s ∩ t) x ↔ unique_diff_within_at 𝕜 s x :=
id     └───────────────────┘         └───────────────────┘   
src    └───────────────────┘             └───────────────────┘
typ    └───────────────────┘         └───────────────────┘   
doc    └───────────────────┘               └───────────────────┘
283  unique_diff_within_at_congr $ (nhds_within_restrict' _ ht).symm
id   └─────────────────────────┘    └───────────────────┘   └┘ └──┘
src  └─────────────────────────┘    └───────────────────┘      └──┘
typ  └─────────────────────────┘    └───────────────────┘   └┘ └──┘
284  
285  lemma unique_diff_within_at.inter (hs : unique_diff_within_at 𝕜 s x) (ht : t ∈ 𝓝 x) :
id                                           └───────────────────┘              
src                                          └───────────────────┘                 
typ                                          └───────────────────┘              
doc                                          └───────────────────┘                  
286    unique_diff_within_at 𝕜 (s ∩ t) x :=
id     └───────────────────┘       
src    └───────────────────┘      
typ    └───────────────────┘       
doc    └───────────────────┘
287  (unique_diff_within_at_inter ht).2 hs
id    └─────────────────────────┘ └┘   └┘
src   └─────────────────────────┘    
typ   └─────────────────────────┘ └┘   └┘
288  
289  lemma unique_diff_within_at_inter' (ht : t ∈ nhds_within x s) :
id                                              └─────────┘  
src                                              └─────────┘
typ                                             └─────────┘  
doc                                               └─────────┘
290    unique_diff_within_at 𝕜 (s ∩ t) x ↔ unique_diff_within_at 𝕜 s x :=
id     └───────────────────┘         └───────────────────┘   
src    └───────────────────┘             └───────────────────┘
typ    └───────────────────┘         └───────────────────┘   
doc    └───────────────────┘               └───────────────────┘
291  unique_diff_within_at_congr $ (nhds_within_restrict'' _ ht).symm
id   └─────────────────────────┘    └────────────────────┘   └┘ └──┘
src  └─────────────────────────┘    └────────────────────┘      └──┘
typ  └─────────────────────────┘    └────────────────────┘   └┘ └──┘
292  
293  lemma unique_diff_within_at.inter' (hs : unique_diff_within_at 𝕜 s x) (ht : t ∈ nhds_within x s) :
id                                            └───────────────────┘             └─────────┘  
src                                           └───────────────────┘                 └─────────┘
typ                                           └───────────────────┘             └─────────┘  
doc                                           └───────────────────┘                  └─────────┘
294    unique_diff_within_at 𝕜 (s ∩ t) x :=
id     └───────────────────┘       
src    └───────────────────┘      
typ    └───────────────────┘       
doc    └───────────────────┘
295  (unique_diff_within_at_inter' ht).2 hs
id    └──────────────────────────┘ └┘   └┘
src   └──────────────────────────┘    
typ   └──────────────────────────┘ └┘   └┘
296  
297  lemma is_open.unique_diff_within_at (hs : is_open s) (xs : x ∈ s) : unique_diff_within_at 𝕜 s x :=
id                                             └─────┘               └───────────────────┘   
src                                            └─────┘                  └───────────────────┘
typ                                            └─────┘               └───────────────────┘   
doc                                            └─────┘                   └───────────────────┘
298  begin
st   └─────
299    have := unique_diff_within_at_univ.inter (mem_nhds_sets hs xs),
id             └──────────────────────────────┘  └───────────┘ └┘ └┘
src    └──────┘└──────────────────────────────┘ └───────────┘    
typ    └──────┘└──────────────────────────────┘ └───────────┘└┘└┘
doc    └──────┘                                                  
txt    └──────┘                                                  
par    └──────┘                                                  
pid    └───┘└─┘                                                  
st   ───────────────────────────────────────────────────────────────┘└─
300    rwa univ_inter at this
id         └────────┘
src    └──┘└────────┘└───────┘
typ    └──┘└────────┘└───────┘
doc    └──┘          └───────┘
txt    └──┘          └───────┘
par    └──┘          └───────┘
pid                 └──────┘
st   ────────────────────────┘
301  end
st   └─┘
302  
303  lemma unique_diff_on.inter (hs : unique_diff_on 𝕜 s) (ht : is_open t) : unique_diff_on 𝕜 (s ∩ t) :=
id                                    └────────────┘          └─────┘     └────────────┘     
src                                   └────────────┘            └─────┘      └────────────┘      
typ                                   └────────────┘          └─────┘     └────────────┘     
doc                                   └────────────┘            └─────┘      └────────────┘
304  λx hx, (hs x hx.1).inter (mem_nhds_sets ht hx.2)
id     └┘   └┘  └┘  └───┘   └───────────┘ └┘ └┘
src                   └───┘   └───────────┘      
typ    └┘   └┘  └┘  └───┘   └───────────┘ └┘ └┘
305  
306  lemma is_open.unique_diff_on (hs : is_open s) : unique_diff_on 𝕜 s :=
id                                      └─────┘     └────────────┘  
src                                     └─────┘      └────────────┘
typ                                     └─────┘     └────────────┘  
doc                                     └─────┘      └────────────┘
307  λx hx, is_open.unique_diff_within_at hs hx
id     └┘  └───────────────────────────┘ └┘ └┘
src         └───────────────────────────┘
typ    └┘  └───────────────────────────┘ └┘ └┘
308  
309  /-- The product of two sets of unique differentiability at points `x` and `y` has unique
310  differentiability at `(x, y)`. -/
311  lemma unique_diff_within_at.prod {t : set F} {y : F}
id                                         └─┘        
src                                        └─┘
typ                                        └─┘        
312    (hs : unique_diff_within_at 𝕜 s x) (ht : unique_diff_within_at 𝕜 t y) :
id           └───────────────────┘           └───────────────────┘   
src          └───────────────────┘              └───────────────────┘
typ          └───────────────────┘           └───────────────────┘   
doc          └───────────────────┘              └───────────────────┘
313    unique_diff_within_at 𝕜 (set.prod s t) (x, y) :=
id     └───────────────────┘   └──────┘      
src    └───────────────────┘    └──────┘      
typ    └───────────────────┘   └──────┘      
doc    └───────────────────┘    └──────┘
314  begin
st   └─────
315    rw [unique_diff_within_at, ← univ_subset_iff] at ⊢ hs ht,
id         └───────────────────┘    └─────────────┘
src    └──┘└───────────────────┘└──┘└─────────────┘└──────────┘
typ    └──┘└───────────────────┘└──┘└─────────────┘└──────────┘
doc    └──┘└───────────────────┘└──┘               └──────────┘
txt    └──┘                     └──┘               └──────────┘
par    └──┘                     └──┘               └──────────┘
pid      └┘                     └──┘               └─────────┘
st   ──────────────────────────┘└─────────────────┘└─────────┘└─
316    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
317    { assume v _,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid      └────────┘
st   ───┘└────────┘└─
318      rw metric.mem_closure_iff',
id          └─────────────────────┘
src      └─┘└─────────────────────┘
typ      └─┘└─────────────────────┘
doc      └─┘└─────────────────────┘
txt      └─┘
par      └─┘
pid        
st   ─────────────────────────────┘└─
319      assume ε ε_pos,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid      └────────────┘
st   ─────────────────┘└─
320      rcases v with ⟨v₁, v₂⟩,
id              
src      └─────┘ └────────────┘
typ      └─────┘└────────────┘
doc      └─────┘ └────────────┘
txt      └─────┘ └────────────┘
par      └─────┘ └────────────┘
pid             └────────────┘
st   ─────────────────────────┘└─
321      rcases metric.mem_closure_iff'.1 (hs.1 (mem_univ v₁)) ε ε_pos with ⟨w₁, w₁_mem, h₁⟩,
id              └─────────────────────┘    └┘    └──────┘ └┘    └───┘
src      └─────┘└─────────────────────┘└─┘   └─┘ └──────┘  └─┘      └────────────────────┘
typ      └─────┘└─────────────────────┘└─┘ └┘└─┘ └──────┘└┘└─┘└───┘└────────────────────┘
doc      └─────┘└─────────────────────┘└─┘   └─┘           └─┘      └────────────────────┘
txt      └─────┘                       └─┘   └─┘           └─┘      └────────────────────┘
par      └─────┘                       └─┘   └─┘           └─┘      └────────────────────┘
pid                                   └─┘   └─┘           └─┘      └────────────────────┘
st   ──────────────────────────────────────────────────────────────────────────────────────┘└─
322      rcases metric.mem_closure_iff'.1 (ht.1 (mem_univ v₂)) ε ε_pos with ⟨w₂, w₂_mem, h₂⟩,
id              └─────────────────────┘    └┘    └──────┘ └┘    └───┘
src      └─────┘└─────────────────────┘└─┘   └─┘ └──────┘  └─┘      └────────────────────┘
typ      └─────┘└─────────────────────┘└─┘ └┘└─┘ └──────┘└┘└─┘└───┘└────────────────────┘
doc      └─────┘└─────────────────────┘└─┘   └─┘           └─┘      └────────────────────┘
txt      └─────┘                       └─┘   └─┘           └─┘      └────────────────────┘
par      └─────┘                       └─┘   └─┘           └─┘      └────────────────────┘
pid                                   └─┘   └─┘           └─┘      └────────────────────┘
st   ──────────────────────────────────────────────────────────────────────────────────────┘└─
323      have I₁ : (w₁, (0 : F)) ∈ submodule.span 𝕜 (tangent_cone_at 𝕜 (set.prod s t) (x, y)),
id                  └┘           └────────────┘    └─────────────┘   └──────┘      
src      └────────┘   └┘ └──┘ └─┘└────────────┘  └─────────────┘  └──────┘  └┘ └┘ └┘
typ      └────────┘ └┘└┘ └──┘└─┘└────────────┘  └─────────────┘ └──────┘└┘└┘└┘
doc      └────────┘   └┘ └──┘ └─┘ └────────────┘  └─────────────┘  └──────┘  └┘  └┘ └┘
txt      └────────┘   └┘ └──┘ └─┘                                            └┘  └┘ └┘
par      └────────┘   └┘ └──┘ └─┘                                            └┘  └┘ └┘
pid      └─────┘└─┘   └┘ └──┘ └─┘                                            └┘  └┘ └┘
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
324      { apply submodule.span_induction w₁_mem,
id               └──────────────────────┘ └────┘
src        └────┘└──────────────────────┘
typ        └────┘└──────────────────────┘└────┘
doc        └────┘└──────────────────────┘
txt        └────┘                        
par        └────┘                        
pid                                     
st   ─────┘└───────────────────────────────────┘└─
325        { assume w hw,
src          └─────────┘
typ          └─────────┘
doc          └─────────┘
txt          └─────────┘
par          └─────────┘
pid          └─────────┘
st   ───────┘└─────────┘└─
326          have : (w, (0 : F)) ∈ (set.prod (tangent_cone_at 𝕜 s x) {(0 : F)}),
id                                └──────┘  └─────────────┘          
src          └─────┘ └┘ └──┘ └─┘  └──────┘ └─────────────┘   └┘ └──┘ └─┘
typ          └─────┘└┘ └──┘ └─┘  └──────┘ └─────────────┘└┘ └──┘└─┘
doc          └─────┘  └┘ └──┘ └─┘  └──────┘ └─────────────┘   └┘  └──┘ └─┘
txt          └─────┘  └┘ └──┘ └─┘                             └┘  └──┘ └─┘
par          └─────┘  └┘ └──┘ └─┘                             └┘  └──┘ └─┘
pid          └───┘└┘  └┘ └──┘ └─┘                             └┘  └──┘ └─┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
327          { rw mem_prod,
id                └──────┘
src            └─┘└──────┘
typ            └─┘└──────┘
doc            └─┘
txt            └─┘
par            └─┘
pid              
st   ─────────┘└─────────┘└─
328            simp [hw],
id                   └┘
src            └────┘  
typ            └────┘└┘
doc            └────┘  
txt            └────┘  
par            └────┘  
pid                  
st   ──────────────────┘└─
329            apply mem_insert },
id                   └────────┘
src            └────┘└────────┘
typ            └────┘└────────┘
doc            └────┘          
txt            └────┘          
par            └────┘          
pid                           
st   ──────────────────────────┘└┘
330          have : (w, (0 : F)) ∈ tangent_cone_at 𝕜 (set.prod s t) (x, y) :=
id                               └─────────────┘   └──────┘      
src          └─────┘  └┘ └──┘ └─┘ └─────────────┘  └──────┘  └┘ └┘ └────
typ          └─────┘ └┘ └──┘└─┘ └─────────────┘ └──────┘└┘└┘└────
doc          └─────┘  └┘ └──┘ └─┘ └─────────────┘  └──────┘  └┘  └┘ └────
txt          └─────┘  └┘ └──┘ └─┘                            └┘  └┘ └────
par          └─────┘  └┘ └──┘ └─┘                            └┘  └┘ └────
pid          └───┘└┘  └┘ └──┘ └─┘                            └┘  └┘ └───
st   ─────────────────────────────────────────────────────────────────────────
331            subset_tangent_cone_prod_left ht.2 this,
id             └───────────────────────────┘ └┘   └──┘
src  ─────────┘└───────────────────────────┘  └─┘
typ  ─────────┘└───────────────────────────┘└┘└─┘└──┘
doc  ─────────┘└───────────────────────────┘  └─┘
txt  ─────────┘                               └─┘
par  ─────────┘                               └─┘
pid  ─────────┘                               └─┘
st   ────────────────────────────────────────────────┘└─
332          exact submodule.subset_span this },
id                 └───────────────────┘ └──┘
src          └────┘└───────────────────┘    
typ          └────┘└───────────────────┘└──┘
doc          └────┘                         
txt          └────┘                         
par          └────┘                         
pid                                        
st   ────────────────────────────────────────┘└┘
333        { exact submodule.zero_mem _ },
id                 └────────────────┘
src          └────┘└────────────────┘└─┘
typ          └────┘└────────────────┘└─┘
doc          └────┘                  └─┘
txt          └────┘                  └─┘
par          └────┘                  └─┘
pid                                 └┘
st   ───────┘└─────────────────────────┘└┘
334        { assume a b ha hb,
src          └──────────────┘
typ          └──────────────┘
doc          └──────────────┘
txt          └──────────────┘
par          └──────────────┘
pid          └──────────────┘
st   ───────┘└──────────────┘└─
335          have : (a, (0 : F)) + (b, (0 : F)) = (a + b, (0 : F)), by simp,
id                                                        
src          └─────┘  └┘ └──┘ └─┘  └┘ └──┘ └─┘   └┘ └──┘ └┘     └──┘
typ          └─────┘  └┘ └──┘ └─┘  └┘ └──┘ └─┘ └┘ └──┘└┘     └──┘
doc          └─────┘  └┘ └──┘ └─┘   └┘ └──┘ └─┘     └┘ └──┘ └┘     └──┘
txt          └─────┘  └┘ └──┘ └─┘   └┘ └──┘ └─┘     └┘ └──┘ └┘     └──┘
par          └─────┘  └┘ └──┘ └─┘   └┘ └──┘ └─┘     └┘ └──┘ └┘     └──┘
pid          └───┘└┘  └┘ └──┘ └─┘   └┘ └──┘ └─┘     └┘ └──┘ └┘
st   ────────────────────────────────────────────────────────────┘         └─
336          rw ← this,
id                └──┘
src          └───┘
typ          └───┘└──┘
doc          └───┘
txt          └───┘
par          └───┘
pid            └─┘
st   ────────────────┘└─
337          exact submodule.add_mem _ ha hb },
id                 └───────────────┘   └┘ └┘
src          └────┘└───────────────┘└─┘    
typ          └────┘└───────────────┘└─┘└┘└┘
doc          └────┘                 └─┘    
txt          └────┘                 └─┘    
par          └────┘                 └─┘    
pid                                └─┘    
st   ───────────────────────────────────────┘└┘
338        { assume c a ha,
src          └───────────┘
typ          └───────────┘
doc          └───────────┘
txt          └───────────┘
par          └───────────┘
pid          └───────────┘
st   ────────────────────┘└─
339          have : c • (0 : F) = (0 : F), by simp,
id                                   
src          └─────┘  └──┘ └┘  └──┘      └──┘
typ          └─────┘ └──┘ └┘  └──┘     └──┘
doc          └─────┘   └──┘ └┘  └──┘      └──┘
txt          └─────┘   └──┘ └┘  └──┘      └──┘
par          └─────┘   └──┘ └┘  └──┘      └──┘
pid          └───┘└┘   └──┘ └┘  └──┘ 
st   ───────────────────────────────────┘         └─
340          rw ← this,
id                └──┘
src          └───┘
typ          └───┘└──┘
doc          └───┘
txt          └───┘
par          └───┘
pid            └─┘
st   ────────────────┘└─
341          exact submodule.smul_mem _ _ ha } },
id                 └────────────────┘     └┘
src          └────┘└────────────────┘└───┘  
typ          └────┘└────────────────┘└───┘└┘
doc          └────┘                  └───┘  
txt          └────┘                  └───┘  
par          └────┘                  └───┘  
pid                                 └───┘  
st   ───────────────────────────────────────┘└──┘
342      have I₂ : ((0 : E), w₂) ∈ submodule.span 𝕜 (tangent_cone_at 𝕜 (set.prod s t) (x, y)),
id                          └┘    └────────────┘    └─────────────┘   └──────┘      
src      └────────┘  └──┘ └─┘  └┘ └────────────┘  └─────────────┘  └──────┘  └┘ └┘ └┘
typ      └────────┘  └──┘└─┘└┘└┘ └────────────┘  └─────────────┘ └──────┘└┘└┘└┘
doc      └────────┘  └──┘ └─┘  └┘ └────────────┘  └─────────────┘  └──────┘  └┘  └┘ └┘
txt      └────────┘  └──┘ └─┘  └┘                                            └┘  └┘ └┘
par      └────────┘  └──┘ └─┘  └┘                                            └┘  └┘ └┘
pid      └─────┘└─┘  └──┘ └─┘  └┘                                            └┘  └┘ └┘
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
343      { apply submodule.span_induction w₂_mem,
id               └──────────────────────┘ └────┘
src        └────┘└──────────────────────┘
typ        └────┘└──────────────────────┘└────┘
doc        └────┘└──────────────────────┘
txt        └────┘                        
par        └────┘                        
pid                                     
st   ─────┘└───────────────────────────────────┘└─
344        { assume w hw,
src          └─────────┘
typ          └─────────┘
doc          └─────────┘
txt          └─────────┘
par          └─────────┘
pid          └─────────┘
st   ───────┘└─────────┘└─
345          have : ((0 : E), w) ∈ (set.prod {(0 : E)} (tangent_cone_at 𝕜 t y)),
id                                └──────┘          └─────────────┘   
src          └─────┘ └──┘ └─┘ └┘  └──────┘ └──┘ └─┘ └─────────────┘   └┘
typ          └─────┘ └──┘ └─┘└┘  └──────┘ └──┘└─┘ └─────────────┘└┘
doc          └─────┘  └──┘ └─┘ └┘  └──────┘  └──┘ └─┘ └─────────────┘   └┘
txt          └─────┘  └──┘ └─┘ └┘            └──┘ └─┘                   └┘
par          └─────┘  └──┘ └─┘ └┘            └──┘ └─┘                   └┘
pid          └───┘└┘  └──┘ └─┘ └┘            └──┘ └─┘                   └┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
346          { rw mem_prod,
id                └──────┘
src              └──────┘
typ              └──────┘
doc             
txt             
par             
st   ────────┘   └──────┘└─
347            simp [hw],
id                   └┘
src                 
typ               └┘
doc                 
txt                 
par                 
pid                   
st   ──────────┘   └─┘ 
348            apply mem_insert },
id                   └────────┘
src            └────┘└────────┘
typ            └────┘└────────┘
doc            └────┘          
txt            └────┘          
par            └────┘          
pid                           
st   ──────────────────────────┘ 
349          have : ((0 : E), w) ∈ tangent_cone_at 𝕜 (set.prod s t) (x, y) :=
id           └┘                 └─────────────┘   └──────┘      
src          └┘                   └─────────────┘    └──────┘      
typ          └┘                 └─────────────┘   └──────┘      
doc          └┘                   └─────────────┘    └──────┘
st          └┘                                                 
350            subset_tangent_cone_prod_right hs.2 this,
id             └────────────────────────────┘ └┘  └──┘
src            └────────────────────────────┘   
typ            └────────────────────────────┘ └┘  └──┘
doc            └────────────────────────────┘
st                        
351          exact submodule.subset_span this },
id                 └┘ └────────────────┘ └──┘
src                └┘ └────────────────┘
typ                └┘ └────────────────┘ └──┘
st                                            └┘
352        { exact submodule.zero_mem _ },
id                 └────────────────┘
src                └────────────────┘
typ                └────────────────┘
st                                      └┘
353        { assume a b ha hb,
354          have : ((0 : E), a) + ((0 : E), b) = ((0 : E), a + b), by simp,
id                                                           
src                                               
typ                                                          
355          rw ← this,
id                └──┘
typ               └──┘
356          exact submodule.add_mem _ ha hb },
id                 └─┘ └───────────┘
src                └─┘ └───────────┘
typ                └─┘ └───────────┘
st                                           └┘
357        { assume c a ha,
358          have : c • (0 : E) = (0 : E), by simp,
id                                    
typ                                   
359          rw ← this,
id                └──┘
typ               └──┘
360          exact submodule.smul_mem _ _ ha } },
id                 └──┘  └────┘  └──┘
src                └──┘  └────┘  └──┘
typ                └──┘  └────┘  └──┘
st                                           └──┘
361      have I : (w₁, w₂) ∈ submodule.span 𝕜 (tangent_cone_at 𝕜 (set.prod s t) (x, y)),
id                 └┘  └┘    └────────────┘    └─────────────┘   └──────┘      
src                          └────────────┘    └─────────────┘    └──────┘      
typ                └┘  └┘    └────────────┘    └─────────────┘   └──────┘      
doc                          └────────────┘    └─────────────┘    └──────┘
362      { have : (w₁, (0 : F)) + ((0 : E), w₂) = (w₁, w₂), by simp,
id                                              └┘  └┘
src                                               
typ                                             └┘  └┘
363        rw ← this,
id              └──┘
typ             └──┘
364        exact submodule.add_mem _ I₁ I₂ },
id               └─┘ └─┘ └───────┘
src              └─┘ └─┘ └───────┘
typ              └─┘ └─┘ └───────┘
st                                         └┘
365      refine ⟨(w₁, w₂), I, _⟩,
id                └┘  └┘   
typ               └┘  └┘   
366      simp [dist, h₁, h₂] },
id                   └┘  └┘
typ                  └┘  └┘
st                           └┘
367    { simp [closure_prod_eq, mem_prod_iff, hs.2, ht.2] }
id             └─────────────┘  └──────────┘  └┘    └┘
src            └─────────────┘  └──────────┘
typ            └─────────────┘  └──────────┘  └┘    └┘
st                                                        └─
368  end
st   ──┘
369  
370  /-- The product of two sets of unique differentiability is a set of unique differentiability. -/
371  lemma unique_diff_on.prod {t : set F} (hs : unique_diff_on 𝕜 s) (ht : unique_diff_on 𝕜 t) :
id                                  └─┘         └────────────┘          └────────────┘  
src                                 └─┘          └────────────┘            └────────────┘
typ                                 └─┘         └────────────┘          └────────────┘  
doc                                              └────────────┘            └────────────┘
372    unique_diff_on 𝕜 (set.prod s t) :=
id     └────────────┘   └──────┘  
src    └────────────┘    └──────┘
typ    └────────────┘   └──────┘  
doc    └────────────┘    └──────┘
373  λ ⟨x, y⟩ h, unique_diff_within_at.prod (hs x h.1) (ht y h.2)
id           └────────────────────────┘  └┘       └┘   
src              └────────────────────────┘                  
typ          └────────────────────────┘  └┘       └┘   
doc              └────────────────────────┘
374  
375  /-- In a real vector space, a convex set with nonempty interior is a set of unique
376  differentiability. -/
377  theorem unique_diff_on_convex {s : set G} (conv : convex s) (hs : (interior s).nonempty) :
id                                      └─┘           └────┘          └──────┘  └──────┘
src                                     └─┘            └────┘           └──────┘   └──────┘
typ                                     └─┘           └────┘          └──────┘  └──────┘
doc                                                    └────┘           └──────┘   └──────┘
378    unique_diff_on ℝ s :=
id     └────────────┘  
src    └────────────┘ 
typ    └────────────┘  
doc    └────────────┘
379  begin
st   └─────
380    assume x xs,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
381    have A : ∀v, ∃a∈ tangent_cone_at ℝ s x, ∃b∈ tangent_cone_at ℝ s x, ∃δ>(0:ℝ), δ • v = b-a,
id                                               └─────────────┘                       
src                                              └─────────────┘                         
typ                                              └─────────────┘                       
doc                                                └─────────────┘
st   ─┘              └─────────────┘   └┘    └─────────────┘   └┘           └─┘
382    { assume v,
383      rcases hs with ⟨y, hy⟩,
384      have ys : y ∈ s := interior_subset hy,
id                          └┘        
src                          └┘        
typ                         └┘        
385      have : ∃(δ : ℝ), 0<δ ∧ y + δ • v ∈ s,
id                                     
typ                                    
386      { by_cases h : ∥v∥ = 0,
id         └──────┘     
src        └──────┘     
typ        └──────┘     
doc        └──────┘
st         └──────┘
387        { exact ⟨1, zero_lt_one, by simp [(norm_eq_zero _).1 h, ys]⟩ },
id                     └─────────┘            └──────────┘       └┘
src                    └─────────┘            └──────────┘   
typ                    └─────────┘            └──────────┘       └┘
st                                                                      └┘
388        { rcases mem_interior.1 hy with ⟨u, us, u_open, yu⟩,
id                  └──────────┘  └┘
src                 └──────────┘
typ                 └──────────┘  └┘
389          rcases metric.is_open_iff.1 u_open y yu with ⟨ε, εpos, hε⟩,
id                  └────────────────┘  └────┘  └┘
src                 └────────────────┘
typ                 └────────────────┘  └────┘  └┘
390          let δ := (ε/2) / ∥v∥,
id                           
src                     
typ                          
391          have δpos : 0 < δ := div_pos (half_pos εpos) (lt_of_le_of_ne (norm_nonneg _) (ne.symm h)),
id                           
typ                          
392          have : y + δ • v ∈ s,
id                           
typ                          
393          { apply us (hε _),
394            rw [metric.mem_ball, dist_eq_norm],
395            calc ∥(y + δ • v) - y ∥ = ∥δ • v∥ : by {congr' 1, abel }
id                                          
typ                                         
st                                                                    └┘
396            ... = ∥δ∥ * ∥v∥ : norm_smul _ _
397            ... = δ * ∥v∥ : by simp only [norm, abs_of_nonneg (le_of_lt δpos)]
398            ... = ε /2 : div_mul_cancel _ h
399            ... < ε : half_lt_self εpos },
id                   
typ                  
st                                         └┘
400          exact ⟨δ, δpos, this⟩ } },
id                  
typ                 
st                                 └──┘
401      rcases this with ⟨δ, δpos, hδ⟩,
402      refine ⟨y-x, _, (y + δ • v) - x, _, δ, δpos, by abel⟩,
id                                        
typ                                       
403      exact mem_tangent_cone_of_segment_subset (conv.segment_subset xs ys),
404      exact mem_tangent_cone_of_segment_subset (conv.segment_subset xs hδ) },
st                                                                            └┘
405    have B : ∀v:G, v ∈ submodule.span ℝ (tangent_cone_at ℝ s x),
id                                                            
typ                                                           
406    { assume v,
407      rcases A v with ⟨a, ha, b, hb, δ, hδ, h⟩,
id                
typ               
408      have : v = δ⁻¹ • (b - a),
id                          
typ                         
409        by { rw [← h, smul_smul, inv_mul_cancel, one_smul], exact (ne_of_gt hδ) },
st                                                                                 └┘
410      rw this,
411      exact submodule.smul_mem _ _
412        (submodule.sub_mem _ (submodule.subset_span hb) (submodule.subset_span ha)) },
st                                                                                     └┘
413    refine ⟨univ_subset_iff.1 (λv hv, subset_closure (B v)), subset_closure xs⟩
id                                 
typ                                
414  end
st   └─┘
415  
416  /-- The real interval `[0, 1]` is a set of unique differentiability. -/
417  lemma unique_diff_on_Icc_zero_one : unique_diff_on ℝ (Icc (0:ℝ) 1) :=
id                                                               
src                                                              
typ                                                              
418  begin
419    apply unique_diff_on_convex (convex_Icc 0 1),
420    have : (1/(2:ℝ)) ∈ interior (Icc (0:ℝ) 1) :=
id                      └──────┘  └─┘
src                     └──────┘  └─┘
typ                     └──────┘  └─┘
doc                       └──────┘  └─┘
st             └┘      └──────┘ └──┘   
421      mem_interior.2 ⟨Ioo (0:ℝ) 1, Ioo_subset_Icc_self, is_open_Ioo, by norm_num, by norm_num⟩,
id       └──────────┘    └─┘          └─────────────────┘  └─────────┘
src      └──────────┘    └─┘          └─────────────────┘  └─────────┘
typ      └──────────┘    └─┘          └─────────────────┘  └─────────┘
doc                      └─┘
st       └──────────┘   └──┘        └─────────────────┘  └─────────┘  └┘              └──────┘
422    exact ⟨_, this⟩
id               └──┘
typ              └──┘
423  end
st   └─┘
424  
425  end unique_diff